00100	VAR: x,y,z;
00200	PRE_OP:m,b,c,f;PRE_PRED:r,a,cl,o,u,t,i,mv,cb;
00300	
00400	AXIOM:
00500	a(x)∧cl(x,y)⊃r(x,y);
00600	o(x,y)∧u(y,b)∧t(y)⊃cl(x,b);
00700	i(x)∧i(y)∧i(z)∧mv(x,y,z)⊃(cl(z,f)∨u(y,z));
00800	cb(x,y)⊃o(x,y);
00900	a(m);
01000	t(c);
01100	i(m);
01200	i(b);
01300	i(c);
01400	mv(m,c,b);
01500	¬cl(b,f);
01600	cb(m,c);
01700	THM: r(m,b);
01800	;